This allows applying constant propagation without upgrading non-constant symbols to L2,
which is useful for the dereferencing logic, as the value-set used to resolve pointer
aliasing is indexed by L1 names.

This may lead to application of array-cell-sensitivity (i.e. querying the symbol
some_array[[1]] instead of some_array[some_index]), leading to higher precision.

Some tests must be amended because better constant propagation causes some test behaviour
to change as symex has better knowledge regarding the targets of pointers.

The use of field_sensitivity for arrays can be expensive for big arrays
so we have to set a limit on the size of constant arrays which get
processed.
The value 64 was determined by changing the size of the array in the
test regression/cbmc/variable-access-to-constant-array and reducing it
until there was no significant difference in execution time between the
versions of CBMC with and without array cell propagation.
For the chosen value the execution time was around 0.05 second in both
cases (for comparison with size 1024 the time with propagation was 0.5
sec, against 0.1 without).

In some cases, like the test in regression/cbmc/Global_Initialization2,
the array type is incomplete and changed in the symbol table after the
main function has been converted, leading to inconsistencies.
This means we can get nil instead of the size in
field_sensitivityt::apply, though the actual size is present in the
symbol table.
The issue is reported here: diffblue#5022

This is to allow constant propagation to take place and know whether the
size is actually constant, which can allow field sensitivity to apply.

When the index is not constant when accessing a constant size array, we
should expand the expression into `{array[0]; array[1];...}[index]` so
that the relation with field sensitivity expressions `array[[0]]`,
`array[[1]]`, etc, is not lost.

This is important to consider dereferenced object as read value.

This may be necessary for constant propagation of the format string.
An example of that is in regression/cbmc/printf1

With field sensitivity on arrays, the element can be initialized in two
steps, first the field f then the field array.

Propagatiof of values of array cells lead to different expressions in VCC.

This is failing because of this bug:
diffblue#4749

Avoid lhs of the form `{array[0], array[1]}[0]`

Most are for C, then a couple are duplicated for Java to check whether its use of a structure
to represent all arrays makes any difference.

This explains how field sensitivity transforms instructions that contain
array operations.

These tests can now be executed in our test suite.

These are companions to the existing tests that check the show-vcc output, and serve to check
that the formulas generated appear to behave properly.

This will allow the user of symex to set this limit as needed instead of
fixing it to an arbitrary value.

together with no-array-field-sensitivity, this makes it possible to
control the maximum size for which the transformation is applied and
totally deactivate field sensitivity for arrays if needed.

This checks that field sensitivity applies or not to arrays depending on
their size and the value of the option.